/*

This is the model of the eXamine description. That is the core of the project,
so the target in this project is to have some confidence of that core.

*/
open util/graph[Component] as graph
open util/graph[Event] as eGraph

abstract sig Event {}
sig ThrownEvent, ReceivedEvent extends Event {}
sig Failure {
	received : set Event,
	thrown : lone ThrownEvent
}
sig Component {}
sig System {
	childs : set Component -> set Component,
	failures : set Component -> set Failure
}

/*
The most important property in the eXamine description is to ensure that
any cicled event is created. But also, establish what events could be received
by a Failure (it's origin).

So this is the list of restrictions & properties associated with the core are:

1. The system (master component) is a tree os sub-components.
2. Received events have the following retrictions:
2.1. A Component Failure can receive simple basic events identified;
2.2. A Component Failure can receive events thrown by sub-components;
2.3. A Component Failure can receive events thrown by same-level-components;
3. The infered event system is a directed acyclic graph.

Some basic properties are already defined at the Alloy signatures.
*/

fun getComponents [ s : System ] : set Component {
	 (s.childs.Component + Component.(s.childs))
}

fun getParent [ s : System, c : Component ] : set Component {
	s.childs.c
}

fun getChilds [ s : System, c : Component ] : set Component {
	c.(s.childs)
}

fun getSameLevel [ s : System, c : Component ] : set Component {
	s.getChilds[s.getParent[c]] - c
}

fun getThrownEvents [ s : System, c : Component ] : set ThrownEvent {
	c.(s.failures.thrown)
}
fun getReceivedEvents [ s : System, c : Component ] : set Event {
	c.(s.failures.received)
}

fun getFailures [ s : System, c : Component ] : set Failure {
	c.(s.failures)
}

fun failureEventGraph [ f : Failure ] : Event -> Event {
	f.received -> f.thrown
}

fun eventGraph [ s : System ] : Event -> Event {
	{ x, y : Event | all c : s.getComponents | x in s.getFailures[c].received && y in s.getFailures[c].thrown }
}

pred isDag [ s : System, f : Failure ] {
	eGraph/dag[eventGraph[s] +  failureEventGraph[f]]
}

pred isDagSystem [ s : System] {
	eGraph/dag[eventGraph[s]]
}

pred isTree [ s : System ] {
	graph/tree[s.childs]
}

pred invSystem [ s : System ] {
	// Requirement 1
	isTree[s]
	// Requirement 2
	all c : s.getComponents | all f : s.getFailures[c] | f.received in (
		// 2.1
		(f.received & ReceivedEvent) +
		// 2.2
		s.getThrownEvents[s.getChilds[c]] +
		// 2.3
		s.getThrownEvents[s.getSameLevel[c]]
	)
	// Requirement 3
	isDagSystem[s]
	// Obvious properties
	// Failures are component dedicated
	all disj c1, c2 : s.getComponents | no c1.(s.failures) & c2.(s.failures)
	// Every failure must receive events
	all f : s.getFailures[s.getComponents] | some f.received
	// Every basic received event are component dedicated
	all disj c1, c2 : s.getComponents | no (s.getReceivedEvents[c1] & ReceivedEvent) & (s.getReceivedEvents[c2] & ReceivedEvent)
	// Thrown events are component dedicated
	all disj c1, c2 : s.getComponents | no s.getThrownEvents[c1] & s.getThrownEvents[c2] 
}

run {
	all s : System | s.invSystem
} for 3 but exactly 1 System, exactly 5 Component

run pretty {
	all s : System | s.invSystem &&
		(all c : Component | c in s.getComponents) &&
		(all f : Failure | f in s.getFailures[s.getComponents]) &&
		(all e : Event | e in s.getFailures[s.getComponents].received + s.getFailures[s.getComponents].thrown)
} for 5 but exactly 1 System, exactly 5 Component
